;;; -*- Mode: Lisp; Package: STELLA; Syntax: COMMON-LISP; Base: 10 -*-

(CL:IN-PACKAGE "STELLA")

(IN-MODULE "/PL-KERNEL-KB/PL-FOUNDATION/PL-SYSTEM")

(IN-DIALECT :KIF)

(set-feature iterative-deepening)

;------------------------------------------------------------------------------
; Basic Definitions
;------------------------------------------------------------------------------

(DEFRELATION  j   ((?x Being) (?y Being))) (ASSERT (closed j))

(DEFRELATION  eps   ((?x Being) (?y Being))
:<=> (
	AND (j ?x Being_U) (j ?x ?y)
)) (ASSERT (closed eps))

(DEFRELATION  c   ((?x Being) (?y Being))
:<=> (
		FORALL ((?z Being)) (
			=> (j ?z ?x) (j ?z ?y)
		)
)) (ASSERT (closed c))

(DEFRELATION  c_   ((?x Being) (?y Being))
:<=> (
		FORALL ((?z Being)) (
			=> (eps ?z ?x) (eps ?z ?y)
		)
)) (ASSERT (closed c_))

(ASSERT (Being Being_V))
(ASSERT (
	FORALL ((?x Being)) (
		<=>
			(eps ?x Being_V)
			(eps ?x ?x)
	)
))

(ASSERT (Being Being_P))
(ASSERT (
	FORALL ((?x Being)) (
		<=>
			(j ?x Being_P)
			(AND (j ?x ?x)(NOT (eps ?x Being_V)))
	)
))

;------------------------------------------------------------------------------
; Axioms
;------------------------------------------------------------------------------

; AP1
(ASSERT (
	FORALL ((?x Being) (?y Being)) ( 
		<=>
			(j ?x ?y)
			(FORALL ((?z Being)) (
				=> (j ?z ?x) (j ?z ?y)
			))
	)
))

; AK1
(ASSERT (
	AND 
		(FORALL ((?y Being)) (EXISTS ((?x Being)) (
					NOT (j ?x ?y)
		)))
		(FORALL ((?x Being)) (EXISTS ((?y Being)) (
					NOT (j ?x ?y)
		)))
))

; Unum - U
(ASSERT (Being Being_U))
(ASSERT (
	FORALL ((?x Being)) (
		<=>
			(j ?x Being_U)
			(FORALL ((?z Being)) (
				=> (j ?z ?x) (j ?x ?z)
			))
	)
))

; AL1
(ASSERT (
	FORALL ((?x Being) (?y Being)) ( 
		=>
			(FORALL ((?z Being)) (
				=>
					(AND (j ?z Being_U)(j ?z ?x))
					(j ?z ?y)
			))
			(FORALL ((?z Being)) (
				=>
					(j ?z ?x)
					(j ?z ?y)
			))
	)
))

; AL2
(ASSERT (
	FORALL ((?x Being)) ( 
		EXISTS ((?z Being)) (
			eps ?z ?x
		)
	)
))

;------------------------------------------------------------------------------
; Aristotle Definitions
;------------------------------------------------------------------------------

(DEFRELATION  i_   ((?x Being) (?y Being))
:<=> (
	EXISTS ((?z Being)) (
		AND
			(eps ?z ?x)
			(eps ?z ?y)
	)
)) (ASSERT (closed i_))

(DEFRELATION  a_   ((?x Being) (?y Being))
:<=> (
	FORALL ((?z Being)) (
		=>
			(eps ?z ?x)
			(i_ ?z ?y)
	)
)) (ASSERT (closed a_))

(DEFRELATION  e_   ((?x Being) (?y Being))
:<=> (
	FORALL ((?z Being)) (
		=>
			(eps ?z ?x)
			(NOT (eps ?z ?y))
	)		
)) (ASSERT (closed e_))

(DEFRELATION  o_   ((?x Being) (?y Being))
:<=> (
	EXISTS ((?z Being)) (
		AND
			(eps ?z ?x)
			(e_ ?z ?y)
	)		
)) (ASSERT (closed o_))

;------------------------------------------------------------------------------
; Additional Definitions
;------------------------------------------------------------------------------

(DEFRELATION  eq  ((?x Being) (?y Being))
:<=> (
	AND (c ?x ?y) (c ?y ?x)
)) (ASSERT (closed eq_))

(DEFRELATION  eq_  ((?x Being) (?y Being))
:<=> (
	AND (c_ ?x ?y) (c_ ?y ?x)
)) (ASSERT (closed eq_))

(DEFRELATION  eq__  ((?x Being) (?y Being))
:<=> (
	AND (eps ?x ?y) (eps ?y ?x)
)) (ASSERT (closed eq__))
